Nuprl Lemma : ecl-kinds_wf
0,22
postcript
pdf
ds
:
x
:Id fp
Type,
da
:
k
:Knd fp
Type,
x
:ecl(
ds
;
da
). ecl-kinds(
x
)
Knd List
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
ecl-kinds(
x
)
,
x
,
y
.
t
(
x
;
y
)
,
x
,
y
,
z
,
w
.
t
(
x
;
y
;
z
;
w
)
,
x
,
y
,
z
.
t
(
x
;
y
;
z
)
,
x
.
t
(
x
)
,
x
(
s1
,
s2
)
,
x
(
s1
,
s2
,
s3
,
s4
)
,
x
(
s1
,
s2
,
s3
)
,
x
(
s
)
Lemmas
ecl
ind
wf
,
decl-state
wf
,
ma-valtype
wf
,
bool
wf
,
append
wf
,
nat
wf
,
ecl
wf
,
fpf
wf
,
Knd
wf
,
Id
wf
origin
ds:x:Id fp
Type, da:k:Knd fp Type, x:ecl(ds;da). ecl-kinds(x) 
Knd List ds:x:Id fp Type, da:k:Knd fp Type, x:ecl(ds;da). ecl-kinds(x) Knd List x:A. B(x) T
x,y. t(x;y)x,y,z,w. t(x;y;z;w)x,y,z. t(x;y;z)x. t(x)